T:Type, L1, L2:T List. L1  L2  L1  L2 

latex

Definitions	x:A. B(x), P  Q, L1  L2, Prop, t  T, ||as||, ij, False, A, AB, , {T}, SQType(T), P & Q, P  Q, x:A. B(x), as @ bs, l1  l2
Lemmas	append wf, le wf, cons one one, nat wf, non neg length, length wf1, sublist wf, member wf, sublist weakening, interleaving sublist, sublist append1